00010	%Interchange sort taken from James King's Ph. D. thesis.%
00020	
00100	PASCAL ENTRY N ≥ 1&SAMESET(A,A0,A[ARBITRARY]);
00200	EXIT ∀K((1≤K)∧(K≤N-1) ⊃ A[K]≤A[K+1])&SAMESET(A,A0,A[ARBITRARY]);
00250	BEGIN J←N;
00300	ASSERT ∀K((J+1≤K)∧(K≤N-1) ⊃ A[K]≤A[K+1]) &
00400	       ∀M((1≤M)∧(M≤J)∧(J≤N-1) ⊃ A[M]≤A[J+1]) &
00500	       1≤J&J≤N & MULTISET(A,A0,J+1,A[J+1],LOC,A[LOC]);
00600	WHILE J ≥2 DO
00700	BEGIN
00800		BIG ← A[1]; LOC ← 1; I ← 2;
00900		ASSERT ∀K((J+1≤K)∧(K≤N-1) ⊃ A[K]≤A[K+1]) &
01000		       ∀L((1≤L)∧(L≤I-1)∧(I-1≤N) ⊃ A[L]≤BIG) &
01100		       ∀M((1≤M)∧(M≤J)∧(J≤N-1) ⊃ A[M]≤A[J+1]) &
01200		       BIG=A[LOC]&1≤LOC&LOC≤J&I≥2 &
01300		       2≤J&J≤N & SAMESET(A,A0,A[ARBITRARY]);
01400		WHILE I≤J DO
01500			BEGIN IF A[I]>BIG THEN
01600				BEGIN BIG←A[I]; LOC←I END;
01700			I←I+1
01800			END;
01900		A[LOC] ← A[J];
02000		A[J] ← BIG;
02100		J←J-1
02200	END
02300	END.;